\begin{tabbing}
interleaving\_occurence($T$;$L_{1}$;$L_{2}$;$L$;$f_{1}$;$f_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\parallel$$L$$\parallel$ $=$ $\parallel$$L_{1}$$\parallel$+$\parallel$$L_{2}$$\parallel$\+
\\[0ex]\& increasing($f_{1}$;$\parallel$$L_{1}$$\parallel$) \& ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$}}$. $L_{1}$[$j$] $=$ $L$[$f_{1}$($j$)])
\\[0ex]\& increasing($f_{2}$;$\parallel$$L_{2}$$\parallel$) \& ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$. $L_{2}$[$j$] $=$ $L$[$f_{2}$($j$)])
\\[0ex]\& ($\forall$$j_{1}$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$}}$, $j_{2}$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$. $\neg$$f_{1}$($j_{1}$) $=$ $f_{2}$($j_{2}$))
\-
\end{tabbing}